import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.ArrayList;

public class TotalTest {
    public static void main(String[] args) {
//        test1();
        test2();
//        D1test();
//        D2test();
//      D3BFtest();
//       D3TFtest1();
//        D3TFtest2();
//        ABFtest();
//        ATFtest();
//        Btest();
//         IItest1();
//         IItest2();
//        AAtest1();
//        AAtest2();
//        EETest1();
//        EETest2();
//        AETest1();
//        AETest2();
    }

    public static void test1(){//[{[{ANY(p1,ANY(pn,r)),Exist(pn,pn)}AA -> ANY(p1,Exist(pn,r))],Exist(p1,ANY(pn,not r))}D3 -> Exist(p1,not p1)]
        UnaryFormula p1=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p1"),false));
        UnaryFormula notp1=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p1"),true));
        UnaryFormula pn=new UnaryFormula(new UnaryLiteral(new UnaryAtom("pn"),false));
        UnaryFormula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));
        UnaryFormula notr=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),true));

        BinaryFormula bf1R=new BinaryFormula(FormulaSign.ANY,pn,r);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p1,bf1R);

        BinaryFormula bf2=new BinaryFormula(FormulaSign.EXIST,pn,pn);

        BinaryFormula bf3R=new BinaryFormula(FormulaSign.ANY,pn,notr);
        BinaryFormula bf3=new BinaryFormula(FormulaSign.EXIST,p1,bf3R);

        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,p1,notp1);

//        System.out.println(bf1);
//        System.out.println(bf2);
//        System.out.println(bf3);
//        System.out.println(conclusion);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));
        proofs.add(new ConclusionProof(bf3));

        var res  = Solve.solveHelper(proofs,conclusion, new UsedCondition());
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test1.tex");
    }
    public static void test2(){//[{[{ANY(p2,Exist(p3,r)),[{[{[{Exist(p1,ANY(pn,not r)),ANY(p1,Exist(p2,r))}D2 ->
        // Exist(Exist(p2,r),ANY(pn,not r))]}I -> Exist(Exist(p2,r),Exist(p2,r))]}II -> Exist(p2,p2)]}D1 ->
        // Exist(p2,Exist(p3,r))]}II -> Exist(p3,p3)]

        UnaryFormula p1=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p1"),false));
        UnaryFormula p2=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p2"),false));
        UnaryFormula p3=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p3"),false));
        UnaryFormula pn=new UnaryFormula(new UnaryLiteral(new UnaryAtom("pn"),false));
        UnaryFormula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));
        UnaryFormula not_r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),true));

        BinaryFormula tf1R=new BinaryFormula(FormulaSign.ANY,pn,not_r);
        BinaryFormula tf1=new BinaryFormula(FormulaSign.EXIST,p1,tf1R);
        BinaryFormula tf2R=new BinaryFormula(FormulaSign.EXIST,p2,r);
        BinaryFormula tf2=new BinaryFormula(FormulaSign.ANY,p1,tf2R);
        BinaryFormula tf3R=new BinaryFormula(FormulaSign.EXIST,p3,r);
        BinaryFormula tf3=new BinaryFormula(FormulaSign.ANY,p2,tf3R);

        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,p3,p3);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(tf1));
        proofs.add(new ConclusionProof(tf2));
        proofs.add(new ConclusionProof(tf3));

        System.out.println(Solve.solveHelper(proofs, conclusion, new UsedCondition()));
        
        var res  = Solve.solveHelper(proofs,conclusion, new UsedCondition());
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test2.tex");
    }

    public static void D1test(){
        UnaryFormula p2=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p2"),false));
        Formula p3=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p3"),false));
        Formula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));

        BinaryFormula f=new BinaryFormula(FormulaSign.EXIST,p3,r);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,p2,f);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p2,p2);
        ArrayList<Proof> D1=new ArrayList<>();
        Proof proof1=new ConclusionProof(f1);
        Proof proof2=new ConclusionProof(f2);
        D1.add(proof2);
        D1.add(proof1);
        //Proof proof=new RuleProof(D1, ProofRule.D1);
        BinaryFormula conR=new BinaryFormula(FormulaSign.EXIST,p3,r);
        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,p2,conR);
        var res  = Solve.solveHelper(D1,conclusion, new UsedCondition());
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");
    }

    public static void D2test(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula p3=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p3"),false));
        Formula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));

        BinaryFormula f=new BinaryFormula(FormulaSign.EXIST,p3,r);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,p,q);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,f);
        ArrayList<Proof> D2=new ArrayList<>();
        Proof proof1=new ConclusionProof(f1);
        Proof proof2=new ConclusionProof(f2);
        D2.add(proof1);
        D2.add(proof2);
        Proof proof=new DerivedProof(D2, ProofRule.D2);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");
    }


    public static void D3BFtest(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        Formula not_l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),true));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,not_l);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,l);
        ArrayList<Proof> D3=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        D3.add(p1);
        D3.add(p2);
        Proof proof=new DerivedProof(D3, ProofRule.D3);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(q,not l),Exist(p,l)}D3 -> Exist(p,not q)]
    }
    public static void D3TFtest1(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        Formula not_b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),true));

        BinaryFormula f1_right=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,f1_right);
        BinaryFormula f2_right=new BinaryFormula(FormulaSign.EXIST,a,not_b);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,f2_right);
        ArrayList<Proof> D3=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        D3.add(p1);
        D3.add(p2);
        Proof proof=new DerivedProof(D3, ProofRule.D3);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(q,ANY(a,b)),Exist(p,Exist(a,not b))}D3 -> Exist(p,not q)]
    }
    public static void D3TFtest2(){//这个test不合规，应该删去
        Formula not_q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),true));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        Formula c=new UnaryFormula(new UnaryLiteral(new UnaryAtom("c"),false));
        Formula d=new UnaryFormula(new UnaryLiteral(new UnaryAtom("d"),false));

        BinaryFormula f1_left=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,f1_left,q);
        BinaryFormula f2_left=new BinaryFormula(FormulaSign.ANY,c,d);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,f2_left,not_q);
        ArrayList<Proof> D3=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        D3.add(p1);
        D3.add(p2);
        Proof proof=new DerivedProof(D3, ProofRule.D3);
        System.out.println(proof);//[{ANY(ANY(a,b),q),Exist(ANY(c,d),not q)}D3 -> Exist(ANY(c,d),Exist(a,not b))]
    }
    public static void ABFtest(){
        Formula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula not_p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),true));
        BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,p,not_p);

        ArrayList<Proof> A=new ArrayList<>();
        Proof p1=new ConclusionProof(bf);
        A.add(p1);

        Proof proof=new DerivedProof(A,ProofRule.A);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(p,not p)}A -> ANY(p,*)]
    }
    public static void ATFtest(){//现在也不合规，应该删去
        Formula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        Formula not_b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),true));

        BinaryFormula f1_left=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula f1_right=new BinaryFormula(FormulaSign.EXIST,a,not_b);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,f1_left,f1_right);

        ArrayList<Proof> A=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        A.add(p1);
        Proof proof=new DerivedProof(A, ProofRule.A);
        System.out.println(proof);//[{ANY(ANY(a,b),Exist(a,not b))}A -> ANY(ANY(a,b),*)]
    }

    public static void Btest(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));

        BinaryFormula f=new BinaryFormula(FormulaSign.EXIST,a,b);
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,p,q);
        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,q,f);
        ArrayList<Proof> B=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        B.add(p1);
        B.add(p2);
        Proof proof=new DerivedProof(B, ProofRule.B);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(q,not l),Exist(p,l)}D3 -> Exist(p,not q)]
    }

    public static void IItest1(){
        Formula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula t=new UnaryFormula(new UnaryLiteral(new UnaryAtom("t"),false));

        BinaryFormula f1_right=new BinaryFormula(FormulaSign.EXIST,q,t);
        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,p,f1_right);

        ArrayList<Proof> II=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        II.add(p1);
        Proof proof=new DerivedProof(II, ProofRule.II);
        var latex = proof.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{Exist(p,Exist(q,t))}II -> Exist(q,q)]
    }
    public static void IItest2(){//此时该测试无效，可以删去
        Formula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula t=new UnaryFormula(new UnaryLiteral(new UnaryAtom("t"),false));
        Formula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));

        BinaryFormula tf_left=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula tf=new BinaryFormula(FormulaSign.EXIST,tf_left,t);
        BinaryFormula f=new BinaryFormula(FormulaSign.EXIST,p,tf);

        ArrayList<Proof> II=new ArrayList<>();
        Proof p1=new ConclusionProof(f);
        II.add(p1);
        Proof proof=new DerivedProof(II, ProofRule.II);
        System.out.println(proof);//[{Exist(p,Exist(ANY(a,b),t))}II -> Exist(ANY(a,b),ANY(a,b))]
    }
    public static void AAtest1(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qn=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qn"),false));
        UnaryFormula t=new UnaryFormula(new UnaryLiteral(new UnaryAtom("t"),false));

        BinaryFormula bfR=new BinaryFormula(FormulaSign.ANY,qn,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.EXIST,q,qn);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.AA);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(p,ANY(qn,t)),Exist(q,qn)}AA -> ANY(p,Exist(q,t))]
    }

    public static void AAtest2(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qn=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qn"),false));
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        UnaryFormula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));

        BinaryFormula t=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula bfR=new BinaryFormula(FormulaSign.ANY,qn,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.EXIST,q,qn);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.AA);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(p,ANY(qn,t)),Exist(q,qn)}AA -> ANY(p,Exist(q,t))]
    }

    public static void EETest1(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qR=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qR"),false));
        UnaryFormula t=new UnaryFormula(new UnaryLiteral(new UnaryAtom("t"),false));

        BinaryFormula bfR=new BinaryFormula(FormulaSign.EXIST,q,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.EXIST,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,q,qR);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.EE);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{Exist(p,Exist(q,t)),ANY(q,qR)}EE -> Exist(p,Exist(qR,t))]
    }

    public static void EETest2(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qR=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qR"),false));
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        UnaryFormula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));

        BinaryFormula t=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula bfR=new BinaryFormula(FormulaSign.EXIST,q,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.EXIST,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,q,qR);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.EE);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");
    }

    public static void AETest1(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qR=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qR"),false));
        UnaryFormula t=new UnaryFormula(new UnaryLiteral(new UnaryAtom("t"),false));

        BinaryFormula bfR=new BinaryFormula(FormulaSign.EXIST,q,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,q,qR);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.AE);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(p,Exist(q,t)),ANY(q,qR)}AE -> ANY(p,Exist(qR,t))]
    }

    public static void AETest2(){
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        UnaryFormula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        UnaryFormula qR=new UnaryFormula(new UnaryLiteral(new UnaryAtom("qR"),false));
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        UnaryFormula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));

        BinaryFormula t=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula bfR=new BinaryFormula(FormulaSign.EXIST,q,t);
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p,bfR);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,q,qR);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));

        var res=new DerivedProof(proofs, ProofRule.AE);
        var latex = res.toLatex();
        LatexSaver.saveLatex(latex, "test.tex");//[{ANY(p,Exist(q,t)),ANY(q,qR)}AE -> ANY(p,Exist(qR,t))]
    }

}
